A:Type, f:(A), L:A List.
(b:A. (b  L)  f(b))  split_tail(L | x.f(x)) = <nil,L>  (A List)(A List) 

latex

Definitions	b, t  T, x:A. B(x), , x(s), Prop, (x  l), P  Q, {T}, P  Q, True, P  Q, P & Q, P  Q, A, b, Unit, if b t else f fi, False
Lemmas	ifthenelse wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, bnot wf, not wf, cons member, l member wf, assert wf, bool wf